Nuprl Lemma : R-aframe-rule
11,40
postcript
pdf
i
:Id,
k
:Knd,
L
:(Id List). Raframe(
i
;
k
;
L
) ||-
es
.@
i
:
k
affects only
L
latex
Definitions
t
T
,
True
,
P
Q
,
R-Feasible(
R
)
,
P
&
Q
,
R
||-
es
.
P
(
es
)
,
x
:
A
.
B
(
x
)
,
Consistent(
R
;
es
)
,
Lemmas
Knd
wf
,
Id
wf
,
event
system
wf
,
Raframe
wf
,
R-consistent
wf
origin
i:Id, k:Knd, L:(Id List). Raframe(i;k;L) ||- es.@i: k affects only L i:Id, k:Knd, L:(Id List). Raframe(i;k;L) ||- es.@i: k affects only L 
T
Qx:A. B(x)